home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Language/OS - Multiplatform Resource Library
/
LANGUAGE OS.iso
/
quintus
/
quintus0.lha
/
work
/
p6b.clin2
< prev
next >
Wrap
Text File
|
1992-04-03
|
1KB
|
52 lines
% In a ring, if x*x*x=x for all x in the ring, then xy=yx for all x and y in
% the ring.
assign(clause_splitting,3).
assign(restricted_equality_transform,0).
assign(support_list,[f]).
assign(time_limit,20000).
set(auto_orient).
set(constrained_rewriting).
set(delete_all_instances).
set(early_tautology_test).
set(early_unit_subsumption).
set(equality_transform).
set(equational_rewrite).
set(group_detection).
set(include_original_clause).
clear(precompute_constraints).
set(replacement).
clear(safe_early_priority_test).
%clear(save_rewrite_rules).
clear(save_unrestricted_normal_form).
set(size_by_clause).
set(slidepriority).
set(outrwr).
set(outcsplit).
set(outtreq).
%set(outrwt).
%set(outCacg).
user_rewrite.
g(1) > f(2).
f(2) > j(2).
end.
axiom_list(sprfn).
j(0,X)=X. % 0 is a left identity for sum
j(X,0)=X. % 0 is a right identity for sum
j(g(X),X)=0. % there exists a left inverse for sum
j(X,g(X))=0. % there exists a right inverse for sum
j(j(X,Y),Z)=j(X,j(Y,Z)). % associativity of addition
j(X,Y)=j(Y,X). % commutatvity of addition
f(f(X,Y),Z)=f(X,f(Y,Z)). % associativity of multiplication
f(X,j(Y,Z))=j(f(X,Y),f(X,Z)). % distributivity axiom
f(j(Y,Z),X)=j(f(Y,X),f(Z,X)). % distribitivity axiom
f(X,f(X,X))=X. % special hypothesis
false :- f(a,b)=f(b,a). % denial of the theorem
end.
end_of_input.